We present the latest major release version 6.0 of the quantified Booleanformula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension ofthe conflict-driven clause learning (CDCL) paradigm implemented in state of theart propositional satisfiability (SAT) solvers. The Q-resolution calculus(QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produceQRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct ofthe solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0implements a variant of QCDCL which is based on a generalization of QRES. Thisgeneralization is due to a set of additional axioms and leaves the originalQ-resolution rules unchanged. The generalization of QRES enables QCDCL topotentially produce exponentially shorter proofs than the traditional variant.We present an overview of the features implemented in DepQBF and report onexperimental results which demonstrate the effectiveness of generalized QRES inQCDCL.
展开▼
